Answer:

PAT does not provide runtime debugger. Nevertheless, you can easily do the debugging using variable range checking, assertions or simulator.

• 1) Explicitly providing the range for the global variables, e.g., var x{1..120};. if the variable's range is out of bound in simulation or verification, PAT will throw runtime exception as the feedback.
• 2) Using assert(condition) process inside your program. Assert(condition) will throw a PAT runtime exception during the execution if the condition is evaluated to be false.
• 3) Writing simple (safety) assertions on global data to check whether they are violated or not, e.g., #assert system |= [] invariant; where invariant can be the desired property you want to guarantee.
• 4) If your model is small, you can quickly using simulator to trace the behaviors of your model or generate the complete state space.

Q2: How do I know that my model is error-free?

Answer:

After finishing your model, you can check the syntax of your model by clicking Check Grammar button. If your model is syntactically correct, PAT will display the parsed model in the output window in the bottom. You can check the parsed model to confirm that your model is the one you want. Note: sometimes, a missing bracket or simple typo can produce a different model.

All module parsers in PAT support error recovery, e.g., they can automatically add missing brackets or remove extra brackets or semi-colons. However, all error recovery information will be displayed as warnings in Error List window (see the Figure below). You need to be careful if there are warnings after parsing, because the error recovery feature may parse the model to a different one than you want. We suggest you to clear out all warnings before doing any analysis.

Q3: When I run the model, PAT crashes like following. What should I do?

Answer:

PAT tries to catch all the exceptions internally. However, if the model gives a stack overflow exception, then PAT cannot catch it. The reason of stack overflow exception is most likely because your model has self-loop like following example. Be careful when using ifa with looping back.

var x = 0;
      P = ifa(x==1) {Skip} else{P};

Q4: Is it possible to imprt new Lib file in local folder?

Answer:

Yes. The complied .dll file can either be inside the Lib folder of the installation folder or the under the same directory with the model file.

Q5: For the following program, can the two processes P() and Q() synchronise on the event a? Then how to make them synchronise on 'a' and preserve the execution of statement block ({x++}) in an atomic fashion?

• var x=0;
• P() = a{x++} -> b -> P();
• Q() = a -> c -> P();
• System() = P() || Q();

Answer:

A intuitive solution is to put the event 'a' and increment statement in a 'atomic' action as follows:

• P() = atomic{a -> update{x++} -> Skip};b -> Skip;
• Q() = a ->  c -> Skip;
• aSystem() = P() || Q();

Then x will be updated right after a is engaged, and a will be synchronised.

The other possible solution could be:

• P() = a -> update{x++} -> a1 -> b -> P();
• Q() = a -> a1 -> c -> P();